C:(IdType), A, B:Type, L2:(tg:Id(AB(C(tg) List))) List, L:(IdLnkt:IdC(t)) List, tg:Id,
a:A, b:B.
{map(x.2of(x);L) = concat(map(tgf.map(x.<1of(tgf),x>;2of(tgf)(a,b));L2))  (tg:IdC(tg)) List
{ (tg  map(p.1of(p);L2))
{ ||filter(ms.1of(2of(ms)) = tg;L)|| = 0} 

latex

Definitions	P  Q, P & Q, P  Q, (x  l), Prop, concat(ll), map(f;as), 1of(t), 2of(t), x. t(x), A, False, P  Q, S  T, Id, x(s), IdLnk, S  T, x:A. B(x), Top, t  T, {T}
Lemmas	top wf, map-concat-filter-lemma1, Id wf, IdLnk wf, pi2 wf, pi1 wf, map wf, concat wf, l member wf, not wf, length zero